\section{Predikátová logika s rovnosťou}

Predikátovú logiku môžeme rozšíriť o nové axiómy, ktoré budú
hovoriť o predikáte ``=''.

\par{Axiómy rovnosti:}
\noindent
\begin{itemize}
%%% {{{
    \item[R1:] ak $x$ je premenná, potom formula $x=x$ je axióma
    \item[R2:] ak $x_1,\dots,x_k, y_1, \dots, y_k$ sú premenné a 
        $f$ je $k$-árny funkčný symbol, potom je axiómou formula
        \begin{equation*}
            (x_1 = y_1) \implies ( (x_2 = y_2) \implies ( \dots
                \implies ((x_k = y_k) \implies
                    [f(x_1,\dots,x_k) = f(y_1,\dots,y_k)] \dots )))
        \end{equation*}
    \item[R3:] ak $x_1,\dots,x_k, y_1, \dots y_k$ sú premenné a 
        $P$ je $k$-árny predikátový symbol, potom je axiómou formula
        \begin{equation*}
            (x_1 = y_1) \implies ( (x_2 = y_2) \implies ( \dots
                \implies ((x_k = y_k) \implies
                    [P(x_1,\dots,x_k) \implies P(y_1,\dots,y_k)] \dots )))
        \end{equation*}
%%% }}}        
\end{itemize}

\begin{priklad}[Teória neostrého čiastočného usporiadania $\le$]
\noindent
%%% {{{
    \begin{itemize}
        \item[1.] $(\forall x) \langle x,x\rangle \in \varphi$ -- identita

        \item[2.] $(\forall x) (\forall y) [
            (\langle x,y \rangle \in \varphi \land
             \langle y,x \rangle \in \varphi) \implies (x=y)]$ -- 
             antisymetrickosť

        \item[3.] $(\forall x) (\forall y) (\forall z)
            [( \langle x,y \rangle \in \varphi \land 
               \langle y,z \rangle \in \varphi) \implies
               \langle x,z \rangle \in \varphi]$ --
               tranzitívnosť\footnote{Pozn.: Axiómu môžeme uvádzať aj
               v ekvivalentnom tvare
                $(\forall x) (\forall y) (\forall z)
                [ \langle x,y \rangle \in \varphi \implies (
                    \langle y,z \rangle \in \varphi \implies
                    \langle x,z \rangle \in \varphi)]$. Inak povedané,
                    $(A \land B) \implies C$ sme nahradili
                    $A \implies (B \implies C)$.
               }
    \end{itemize}
    Ak pridáme trichotomickosť, dostaneme teóriu neostrého
    usporiadania:
    \begin{itemize}
        \item[4.] $(\forall x) (\forall y) [x \not=y \implies
            (\langle x,y \rangle \in \varphi \lor 
             \langle y,x \rangle \in \varphi)]$

        \item[4'] $(\forall x) (\forall y) [x = y \lor
             \langle x,y \rangle \in \varphi \lor 
             \langle y,x \rangle \in \varphi]$
    \end{itemize}
%%% }}}    
\end{priklad}

\begin{lema}
Rovnosť je symetrická a tranzitívna.
    \begin{itemize}
        \item[1] $\provable (x=y) \implies (y=x)$ -- symetria
        \item[2] $\provable (x=y) \implies ((y=z) \implies (x=z))$ --
            tranzitívnosť
    \end{itemize}
\end{lema}
\begin{dokaz}
%%% {{{
\noindent
\begin{itemize}
    \item Symetria:
        \begin{itemize}
        \item[1] $\provable (x=y) \implies ((x=x) \implies ((x=x)
                \implies (y=x)))$
            pretože \\
                $\provable (x_1=y_1) \implies ((x_2=y_2) \implies
                    ((x_1=x_2) \implies (y_1=y_2)))$ je inštancia R3
        \item[2] $\provable A \implies (B \implies (B \implies C))$.
        \item[3] $\provable B \implies (B \implies (A \implies C))$ --
            2x použité pravidlo zámeny predpokladov + veta o dedukcii
        \item[4] $\provable (x=x) \implies (x=x) \implies (x=y)
                    \implies (y=x)$
        \item[5] $\provable x=x$ -- R1
        \item[6] $\provable (x=y) \implies (y=x)$ -- 2x MP na 5,4
        \end{itemize}

    \item Tranzitívnosť:
        \begin{itemize}
            \item[1] $\provable (y=x) \implies ((z=z) \implies
                ((y=z) \implies (x=z)))$, pretože \\
                $\provable (x_1 = y_1) \implies ((x_2=y_2) \implies
                 ((x_1=x_2) \implies (y_1=y_2)))$ je inštancia R3.
            \item[2] $\provable A \implies (B \implies (C \implies D))$
            \item[3] $\provable B \implies (A \implies (C \implies D))$
                -- pravidlo zámeny predpokladov
            \item[4] $\provable \highlightc{(z=z)} \implies [
                \highlightp{(y=x) \implies ((y=z) \implies
                (x=z))}]$
            \item[5] $\provable \highlightc{z=z}$ -- R1
            \item[6] $\provable \highlightp{
                    (y=x) \implies ((y=z) \implies (x=z))}$
                -- MP 4,5
            \item[7] $\provable (A \implies B) \implies ((B \implies
                C)) \implies (A \implies C))$ -- JS
            \item[8] $\provable \highlighta{[(x=y) \implies (y=x)]}
                \implies \Big[\highlightb{
                [\highlightp{(y=x) \implies ((y=z) \implies (x=z))}] \implies
                [\highlighto{(x=y) \implies ((y=z) \implies (x=z)))}]} \Big]$ 
                -- inštancia 7
            \item[9] $\provable \highlighta{(x=y) \implies (y=x)}$ -- symetria
            \item[10] $\provable \highlightb{ \highlightp{
                [(y=x) \implies ((y=z) \implies (x=z))]} \implies
                [\highlighto{
                (x=y) \implies ((y=z) \implies (x=z))}]}$ -- MP 9,8
            \item[11] $\provable \highlighto{
                (x=y) \implies ((y=z) \implies (x=z))}$ -- MP 6,10
        \end{itemize}
\end{itemize}
%%% }}}
\end{dokaz}

\begin{veta}
    Nech $t_1,\ldots,t_n,s_1,\ldots,s_n$ sú termy, pričom platí
        $\forall i \in \{1,\dots,n\}:\; \provable t_i = s_i$.
    Potom
    \begin{itemize}
    \item[i)] Ak $t$ je term, ktorý vznikne z termu $s$ nahradením
        niektorých výskytov termov $s_i$ za $t_i$, potom 
        $\provable t=s$.
    \item[ii)] Ak $A'$ je formula, ktorá vznikne z formuly $A$
    dosadením $t_i$ za niektoré termy $s_i$, okrem prípadov, keď
    $t_i$ je premenná $x$ v kvantifikácii $(\forall x)$ 
    resp. $(\exists x)$. Potom
    $\provable A \lequiv A'$.
    \end{itemize}
\end{veta}

\begin{dokaz}
%%% {{{
\noindent
\begin{itemize}
    \item[i)] Dôkaz matematickou indukciou vzhľadom na zložitosť termu $t$.
        %%% {{{
        \begin{itemize}
        \item Nech $t$ je premenná alebo $t$ je $s_i$ pre nejaké $i$.
            Potom zjavne $\provable t=s_i$.

        \item Nech term $t$ je $f(r_1,\dots,r_k)$, 
            term $s$ je $f(r_1',\dots,r_k')$.
            Pre $r_1,\dots,r_k$ platí IP, čize $\provable r_i = r_i'$.
            Potom $\provable (r_1=r_1') \implies  \dots \implies
                (r_k = r_k') \implies (f(r_1,\dots,r_k) = f(r_1',
                    \dots, r_k'))$, čo $k$-násobným použitím MP na 
                    indukčný predpoklad vedie k
                    $\provable f(r_1,\dots,r_k) = f(r_1', \dots,
                    r_k')$.
                
        \end{itemize}
        %%% }}}
    \item[ii)] Zámena termov prebieha len v atomických podformulách
        formuly $A$ (každý term je časťou nejakej atomickej podformuly).
        Máme 2 možnosti, ako vyzerá atomická podformula:
        %%% {{{
        \begin{itemize}
        \item Nech $P$ je atomická podformula tvaru
            $P(r_1,\dots,r_l)$. Potom po zámene dostaneme z 
            $P(r_1, \dots, r_k)$ formulu $P':P(r_1',\dots,r_k')$.
            Chceme ukázať $\provable P(r_1,\dots,r_k) \lequiv
                                     P(r_1',\dots,r_k')$, ak vieme, že
            podľa IP platí $\forall i: \provable r_i = r_i'$
            %%% {{{
            \begin{itemize}
            \item [$\Rightarrow:$] 
                \begin{itemize}
                \item $\provable (r_1=r_1') \implies
                                 (r_2=r_2') \implies \dots \implies
                                 (r_k=r_k') \implies
                                 (P(r_1,\dots,r_k) \implies
                                 P(r_1',\dots,r_k'))$ -- inštancia R3
                \item $\provable r_i = r_i'$ -- IP
                \item $\provable P(r_1,\dots,r_k) \implies
                    P(r_1',\dots, r_k')$ -- $k$-krát MP
                \end{itemize}
            \item [$\Leftarrow:$]
                \begin{itemize}
                \item $\provable (r_1'=r_1) \implies
                                 (r_2'=r_2) \implies \dots \implies
                                 (r_k'=r_k) \implies
                                 (P(r_1',\dots,r_k') \implies
                                 P(r_1,\dots,r_k))$ -- inštancia R3
                \item $\provable r_i' = r_i$ -- IP + symetria
                \item $\provable P(r_1',\dots,r_k') \implies
                    P(r_1,\dots, r_k)$ -- $k$-krát MP
                
                \end{itemize}
            \end{itemize}
            %%% }}}
        \item Nech atomická podformula je tvaru $r_1 = r_2$. 
        Tento prípad sa dá ukázať podobne ako predchádzajúci,
        na prednáške bol ale iný dokaz:
        Chceme ukázať $\provable r_1=r_2 \lequiv r_1'=r_2'$.
            %%% {{{
            \begin{itemize}
            \item[$\Rightarrow:$]
                \begin{itemize}
                \item $\provable r_1=r_1'$ -- IP
                \item $\provable r_2=r_2'$ -- IP
                \item $\provable r_1 = r_2 \implies (
                            r_2 = r_2' \implies r_1 = r_2')$ --
                            tranzitívnosť
                \item $r_1=r_2 \provable r_1=r_2'$ -- VD + MP
                \item $r_1=r_2 \provable r_2'=r_1$ -- symetria + MP
                \item $\provable r_2' = r_1 \implies (
                            r_1 = r_1' \implies r_2' = r_1')$ --
                            tranzitívnosť
                \item $r_1=r_2 \provable r_2' = r_1'$ -- 2-krát MP
                \item $r_1=r_2 \provable r_1' = r_2'$ -- symetria + MP
                \item $\provable r_1=r_2 \implies r_1'=r_2'$ -- VD
                \end{itemize}
            \item[$\Leftarrow:$]
                \begin{itemize}
                \item $\provable r_1=r_1'$ -- IP
                \item $\provable r_2=r_2'$ -- IP
                \item $\provable r_1' = r_2' \implies (
                            r_2' = r_2 \implies r_1' = r_2)$ --
                            tranzitívnosť
                \item $r_1'=r_2' \provable r_1'=r_2$ -- VD + MP
                \item $\provable r_1 = r_1' \implies (
                            r_1' = r_2 \implies r_1 = r_2)$ --
                            tranzitívnosť
                \item $r_1'=r_2' \provable r_1 = r_2$ -- 2xMP
                \item $\provable r_1'=r_2' \implies r_1=r_2$ -- VD
                \end{itemize}
            \end{itemize}
            %%% }}}
        \end{itemize}
        %%% }}}
        Dokázali sme, že atomické podformuly sú ekvivalentné. Spolu s
        vetou o ekvivalencii to ale znamená, že aj pôvodné formuly sú
        ekvivalentné.
\end{itemize}
%%% }}}
\end{dokaz}

\begin{veta}
    Majme term $t$, termy $t_1,\dots,t_n, s_1,\dots, s_n$ a formulu
    $A$.
    Potom platí
    \begin{itemize}
        \item[i)] $\provable t_1=s_2 \implies t_2=s_2 \implies
            t_n=s_n \implies (t[t_1,\dots,t_n] = t[s_1,\dots,s_n])$.
        \item[ii)] $\provable t_1=s_2 \implies t_2=s_2 \implies
            t_n=s_n \implies (A[t_1,\dots,t_n] \lequiv 
                              A[s_1,\dots,s_n])$.
    \end{itemize}
    Ak navyše $x$ je premenná, ktorá nie je obsiahnutá v terme $t$,
    potom platí
    \begin{itemize}
        \item[iii)] $\provable A_x[t] \lequiv 
            (\forall x)((x=t) \implies A)$
        \item[iv)] $\provable A_x[t] \lequiv 
            (\exists x)((x=t) \land A)$
    \end{itemize}
\end{veta}
\begin{dokaz}
    \noindent
    \begin{itemize}
        \item[i),ii)] Ak $t_1,\dots,t_n,s_1,\dots,s_n$ neobsahujú
            premenné, tak to vyplýva priamo z predchádzajúcej vety a vety
            o dedukcii. V prípade, že tieto termy obsahujú premenné,
            tieto premenné nahradíme rôznymi konštantami, použijeme
            vetu o konštantách,\footnote{Veta o konštantách hovorí, že
            $T \provable A \iff T \provable A[c_1,\dots,c_m]$ kde
            $c_1,\dots,c_m$ sú nové konštanty. Inak povedané,
            to, že niečo vieme dokázať s premennými je ekvivalentné
            tomu, že to vieme dokázať ak premenné nahradíme novými
            konštantami} predchádzajúcu vetu a vetu o dedukcii.
        \item[iii)]
            %%% {{{
            \begin{itemize}
            \item[$\Rightarrow:$]
                \begin{itemize}
                \item $\provable x=t \implies (A \lequiv
                    A_x[t])$ -- podľa ii).
                \item $\provable \underbrace{x=t}_X \implies (
                    \underbrace{A_x[t]}_Y \implies
                    \underbrace{A}_Z)$ -- platí totiž
                    $\provable (B \implies (C \lequiv D))
                    \implies (B \implies (D \implies C))$
                \item $(X \implies (Y \implies Z)) \implies
                       (Y \implies (X \implies Z))$ -- pravidlo zámeny
                       predpokladov
                \item $\provable A_x[t] \implies (x=t \implies A)$ --
                    MP na pravidlo zámeny predpokladov
                \item $\provable A_x[t] \implies (\forall x)(x=t
                    \implies A)$ -- pravidlo zavedenia všeobecného
                    kvantifikátora
                \end{itemize}

            \item[$\Leftarrow:$]
                \begin{itemize}
                \item $\provable \underbrace{(\forall x)(x=t \implies
                    A)}_X \implies
                        (\underbrace{(t=t)}_Y \implies
                        \underbrace{A_x[t]}_Z)$ -- Axióma špecifikácie

                \item $(X \implies (Y \implies Z)) \implies
                       (Y \implies (X \implies Z))$ -- pravidlo zámeny
                       predpokladov

                \item $\provable (t=t) \implies ((\forall x) ((x=t)
                    \implies A) \implies A_x[t])$ -- MP

                \item $\provable t=t$ -- axióma R1

                \item $\provable (\forall x) ((x=t)
                    \implies A) \implies A_x[t]$ -- MP
                \end{itemize}
            \end{itemize}
            %%% }}}
        \item[iv)]
            \begin{itemize}
            \item[1] $\provable (\forall x)((x=t) \implies A)
                \lequiv A_x[t]$ -- iii)
            \item[2] $\provable (\forall x)((x=t) \implies \neg A)
                \lequiv \neg A_x[t]$ -- inštancia 1
            \item[3] $\provable \neg \neg A_x[t] \lequiv
                \neg (\forall x) ((x=t) \implies \neg A)$ -- obmena
                ekvivalencie
            \item[4] $\provable A_x[t] \lequiv (\exists x) \neg
                ((x=t) \implies \neg A)$ -- odstránenie $\neg \neg$ a
                zámena kvantifikátora
            \item[5] $\provable \neg(X \implies \neg Y)
                \lequiv  (X \land Y)$ -- rozpísanie
                $\land$
            \item[6] $\provable A_x[t] \lequiv (\exists x)
                ((x=t) \land A)$ -- veta o ekvivalencii aplikovaná na
                4,5

            \end{itemize}
    \end{itemize}
\end{dokaz}

